/* Benchmarks for the PointerC verifier. */

// insert a node to a binary search tree 

struct tree
{
  int data;
  struct tree* l;
  struct tree* r;
};

/*@ let tree(t) = (t==null) ||
  @  	          (({t}) && tree(t->l) && tree(t->l))
  @ in  tree(t)
  @ end
  @*/
struct tree * insert (struct tree * t, int key)
{
  struct tree * q;
  q = null;

  if (t==null)
  {
    t = alloc (struct tree);
    t->data = key;
    t->l = null;
    t->r = null;
  } 
  else
  { 
    if (key >= t->data)
      {
        q = insert (t->r, key);
        t->r = q;
      } else
      {
        q = insert (t->l, key);
        t->l = q;
      }
  }
  return t;
}
/*@ */
